COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	(proof lose)
C00004 ENDMK
C⊗;
(proof lose)

(define equiv |∀e.equiv e ≡ (∀x.e(x,x)) ∧ (∀x y.e(x,y) ⊃ e(y,x))
	∧ (∀x y z.e(x,y) ∧ e(y,z) ⊃ e(x,z))|)

(define e11 |∀x y.e11(x,y) ≡ x = a ∧ y = b ∨ x=b ∧ y=a ∨ x = y|)

(der |equiv e11| nil (open equiv) (open e11))
; ran 5 minutes without result

(define reflexive |∀e. reflexive e ≡ ∀x.e(x,x)|)

(define symmetric |∀e. symmetric e ≡ ∀x y.e(x,y) ⊃ e(y,x)|)

(define transitive |∀e.transitive e ≡ ∀x y z.e(x,y) ∧ e(y,z) ⊃ e(x,z)|)

(der |reflexive e11| nil (open reflexive) (open e11))
; got it immediately

(der |symmetric e11| nil (open symmetric) (open e11))
; took 2 minutes but got it

(der |transitive e11| nil (open transitive) (open e11))
; ran 5 minutes without result

(define equiv |∀e.equiv e ≡ reflexive e ∧ symmetric e ∧ transitive e|)
; not used
jk
more slowness
lose.lsp[s84,jmc] is adapted from equal.lsp[s84,jmc] and shows  DERIVE
taking a long time when asked to show that a simply defined relation
E11 is an equivalence relation.  After it ran 5 minutes without result
using the full definition, I tried it on reflexivity, symmetry and
transitivity separately.  Reflexivity was immediate, symmetry took
almost two minutes, and it didn't get transitivity in 5 minutes.